• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文OA文献 >Development and evaluation of Formula Editor (a tool-based approach to enhance reusability in software product line model checking) on SAFER case study
【2h】

Development and evaluation of Formula Editor (a tool-based approach to enhance reusability in software product line model checking) on SAFER case study

机译：在SAFER案例研究中开发和评估公式编辑器（一种基于工具的方法来增强软件产品线模型检查的可重用性）

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务，本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文，但由于OA文献来源多样且变更频繁，仍可能出现获取不到、文献不完整或与标题不符等情况，如果获取不到我们将提供退款服务。请知悉。
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Although model checking is extensively used for verification of single software systems, currently there is insufficient support for model checking in product lines. The presence of commonalities within the different products in the product line requires that the properties and the corresponding specifications for these properties be verified for every product in the product line. Specification and management of properties for every product in a product line can incur high overhead and make the task of model checking very difficult. It is hence essential to exploit the presence of commonalities to our advantage by providing reusability in model checking of product lines. Since different products in the product line need to be checked for same or similar properties, reuse of properties specified for one product for other products within a product line will significantly reduce the overall property specification and verification time.FormulaEditor is a property specification and management tool for enhancing the reusability of model checking of software product lines. The core of the technique is a product line-oriented user interface to guide users in generating, selecting, managing, and reusing useful product line properties, and patterns of properties for model checking. The previous version of the FormulaEditor tool supports Cadence SMV models, but not the typical CMU-SMV models. This work extends the FormulaEditor tool to allow verification of models written in CMU-SMV. The advantage of providing support to another model checker is twofold: first, it enhances the tool\u27s capability to check design specifications written in different models; and second, it allows users to specify the same design in different modeling languages to detect problems.
机译：尽管模型检查已广泛用于单个软件系统的验证，但目前尚不足以支持产品线中的模型检查。产品线中不同产品之间存在共性，因此需要对产品线中的每个产品的特性和这些特性的相应规格进行验证。对产品线中每个产品的属性进行规范和管理可能会导致高昂的开销，并使模型检查任务非常困难。因此，至关重要的是，通过在产品线模型检查中提供可重用性，来利用通用性对我们有利。由于需要检查产品线中的不同产品是否具有相同或相似的属性，因此为一个产品线中的其他产品重复使用为一种产品指定的属性，将显着减少总体属性规范和验证时间。FormulaEditor是属性规范和管理工具用于增强软件产品线模型检查的可重用性。该技术的核心是面向产品线的用户界面，可以指导用户生成，选择，管理和重用有用的产品线属性以及用于模型检查的属性模式。 FormulaEditor工具的早期版本支持Cadence SMV模型，但不支持典型的CMU-SMV模型。这项工作扩展了FormulaEditor工具，以允许验证以CMU-SMV编写的模型。为另一个模型检查器提供支持的优点是双重的：首先，它增强了该工具检查不同模型中编写的设计规范的能力。其次，它允许用户以不同的建模语言指定相同的设计以检测问题。

著录项

  • 作者

    Krishnan, Sandeep;

  • 作者单位
  • 年度 2009
  • 总页数
  • 原文格式 PDF
  • 正文语种 en
  • 中图分类

相似文献

  • 外文文献
  • 中文文献
  • 专利
代理获取

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号